'''
This file is part of Lampy.

Lampy is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.

Lampy is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with Lampy.  If not, see <http://www.gnu.org/licenses/>.

Copyright 2011 Kevin Han
'''

"""
Reduce lambda calculus expressions.

Variable names mean things:
node: any result of parser.parse()
body: a list of nodes, usually the body of a function
params: a string of characters; the parameters of a function
func: a list [params, body]
name: a character
"""
from string import ascii_letters as CHARS

from utils import *
import integer

def getNewName(name, forbidden):
    """
    Return value for name not in forbidden. This could be name if name is not in
    forbidden.
    """
    if name not in forbidden:
        return name

    new = name
    while True:
        new = CHARS[(CHARS.index(new) + 1) % len(CHARS)]
        if new not in forbidden:
            return new
        if new == name:
            raise ValueError, 'no new name possible'

def substitute(body, nameToNew):
    """
    Return body with all names converted according to the mapping in nameToNew,
    unless the name is in an inner function's parameters.
    """
    newBody = []
    for node in body:
        if isFunc(node):
            innerParams, innerBody = splitFunc(node)
            innerNameToNew = dict(nameToNew)
            # remove all the names that exist in innerParams
            for name in innerParams:
                try:
                    del innerNameToNew[name]
                except KeyError:
                    pass
            newBody.append(makeFunc(
                    innerParams,
                    substitute(innerBody, innerNameToNew)
                    ))
        elif isCompound(node):
            newBody.append(substitute(node, nameToNew))
        elif node in nameToNew:
            newBody.append(nameToNew[node])
        else:
            newBody.append(node)

    return newBody

def reduceOnce(node):
    """
    Reduce an expression once; this basically means performing one round of
    beta-reduction on all the first-level nodes.

    >>> reduceOnce([['/x', 'x'], 'x'])
    'x'
    >>> reduceOnce([['/xyz', [['/x', ['x', 'y']], 'y', 'z', 'x']], [['/y', 'y'], 'y', 'x']])
    None
    >>> reduceOnce(['/x', ['/y', ['x', 'y']]])
    ['/xy', ['x', 'y']]
    """
    if isName(node):
        return node

    if isFunc(node):
        params, body = splitFunc(node)
        # uncurry function if needed
        if isFunc(body):
            innerParams, innerBody = splitFunc(body)
            params += innerParams
            body = innerBody
        return makeFunc(params, reduceOnce(body))

    i = 0
    newNode = []
    while i < len(node):
        innerNode = node[i]
        if isFunc(innerNode):
            params, body = splitFunc(innerNode)

            args = node[i + 1: i + 1 + len(params)]
            args = [reduceOnce(arg) for arg in args]

            if not args:
                newNode.append(innerNode)
            else:
                newNode.append(applyFunc(innerNode, args))
            i += len(params)
        else:
            newNode.append(reduceOnce(innerNode))
        i += 1

    return newNode if len(newNode) > 1 else newNode[0]

def applyFunc(func, args):
    """
    Perform beta-reduction with optional alpha-conversion if needed.

    >>> applyFunc(['/xyz', ['x', 'y', 'z']], ['z'])
    None

    >>> applyFunc(['/xyz', ['x', 'y', 'a']], ['a'])
    ['/yz', ['a', 'y', 'a']]

    >>> applyFunc(['/xyz', ['x', 'y', 'z']], ['z', 'z', 'z'])
    ['z', 'z', 'z']

    >>> applyFunc(['/xyz', [['/x', ['x', 'y']], 'y', 'z', 'x']],
    ... [[['/y', 'y'], 'y', 'x']])
    None
    """
    params, body = splitFunc(func)

    argNames = getNames(args)

    paramToArg = dict(zip(params, args))

    extraParams = params[len(args):]
    # replace all the parameters that occur in the arguments and aren't bound to
    # a value
    toReplace = set(extraParams) & argNames

    bodyNames = getNames(body, withFuncParams=True)

    replacedToNew = dict()
    for replaced in toReplace:
        replacedToNew[replaced] = getNewName(
                replaced,
                bodyNames | set(params) | set(replacedToNew.values())
                )
    # treat the replacement parameters as regular arguments
    paramToArg.update(replacedToNew)

    # perform the replacement
    newBody = substitute(body, paramToArg)
    if extraParams:
        newParams = ''.join(substitute(list(extraParams), paramToArg))
        return makeFunc(newParams, newBody)
    else:
        return newBody if len(newBody) > 1 else newBody[0]

def getNames(node, withFuncParams=False, withFuncBodies=True):
    """
    Return a set of names contained in node.
    
    If withFuncParams, include function parameters.

    If withFuncBodies, include names in function bodies that aren't parameters.
    """
    if isName(node):
        return set(node)
    elif isFunc(node):
        params, body = splitFunc(node)

        result = set()
        if withFuncParams:
            result |= set(params)
        if withFuncBodies:
            result |= getNames(body, withFuncParams, withFuncBodies) \
                    - set(params)
        return result

    return reduce(
            set.union,
            (getNames(innerNode, withFuncParams, withFuncBodies) \
                    for innerNode in node),
            set()
            )

def reduceNode(node, getSteps=False):
    """
    Return the node reduced as much as possible.
    
    If getSteps, return a list of nodes showing each reduction step, including
    the input and final node.
    """
    nodes = [node]
    while True:
        newNode = reduceOnce(node)
        if node == newNode:
            if getSteps:
                return nodes
            else:
                return node
        node = newNode
        nodes.append(newNode)

def getNodeHash(node):
    """
    Return a hashable value unique for each node.
    """
    if isName(node):
        return node

    i = integer.fromNode(node)
    if i is not None:
        return i

    return hashlib.md5(str(node)).hexdigest()

def reduceWithMemo(node, getSteps=False):
    """Same as reducer.reduceNode(), but with memoization."""
    nodeHash = getNodeHash(node)

    try:
        # the cache contains the answer if it's possible to reduce it, or else
        # None if it encountered a recursion error.
        answer = reduceWithMemo.cache[nodeHash]
        if answer is None:
            raise RuntimeError
        return answer
    except AttributeError:
        reduceWithMemo.cache = dict()
    except KeyError:
        pass

    try:
        answer = reduceNode(node, getSteps=getSteps)
    except RuntimeError:
        reduceWithMemo.cache[nodeHash] = None
        raise
    else:
        reduceWithMemo.cache[nodeHash] = answer
        return answer
        
if __name__ == '__main__':
    import doctest

    import parser

    # doctest is used here, but should return errors.
    
    # Because some outputs are not guaranteed to be a certain expression but
    # instead satisfy certain properties (like some in applyFunc()), they should
    # be verified by hand.
    
    # These are indicated by None as a "correct" output.
    doctest.testmod()

    while True:
        try:
            print parser.unparse(
                    reduceNode(parser.parse(raw_input('>>> ')))
                    )
        except Exception as err:
            print 'Error:', err

